#include <vector>
#include <string>
#include <iostream>
#include <fstream>
#include <queue>
#include "cfa.h"
using namespace std;

//extern vector<Prog*> fun;
//extern Prog* prog1;

bool UniNode::operator==(Node &other){
    Node* t = &other;
    if(typeid(*t) == typeid(UniNode)){
        if(((UniNode*)t)->e1 == ((UniNode*)this)->e1 && \
           ((UniNode*)t)->e2 == ((UniNode*)this)->e2 ){
            return true;
        }
        else{
            return false;
        }
    }
    else{
        return false;
    }
}
bool BinNode::operator==(Node &other){
    Node* t = &other;
    if(typeid(*t) == typeid(BinNode)){
        if(((BinNode*)t)->p == ((BinNode*)this)->p){
            return true;
        }
        else{
            return false;
        }
    }
    else{
        return false;
    }
}
bool BadNode::operator==(Node &other){
    Node* t = &other;
    if(typeid(*t) == typeid(BadNode)){
        return true;
    }
    else{
        return false;
    }
}

InequProp* CFA::AssignExpr2Prop(Expr* e1, Expr* e2){
    InequProp* p1 = new InequProp;
    p1->e1 = e1;
    p1->e2 = e2;
    p1->p = Eq;
    return p1;
}
void CFA::ConnectGoto(map<Node*, char*>* gotolist){
    int i1, Flag;
    Node *bn;
    queue<Node*> visited, unvisited;
    map<Node*, char*>::iterator it;
    map<Node*, char*>::iterator label_it;
    for(it = gotolist->begin(); it != gotolist->end(); it++){
        //初始化
        Flag = 0;
        while(!visited.empty()){ visited.pop(); }
        while(!unvisited.empty()){ unvisited.pop(); }
        if(strcmp(it->second, "break") == 0){
            //BFS
            unvisited.push(it->first);
	    while(!unvisited.empty()){
                bn = (unvisited.front());
                for(i1 = 0; i1 < (int)bn->before.size(); i1++){
                    unvisited.push(bn->before[i1]);
                }
                for(i1 = 0; i1 < (int)LoopStart.size(); i1++){
                    if(LoopStart[i1] == bn){
                        Flag = 1;
                        ((UniNode*)it->first)->next = *LoopEnd[i1];
                        cout << "break = " << *LoopEnd[i1] << endl;
                        break;
                    }
                }
                if(Flag == 1){
                    break;
                }
                visited.push(bn);
                unvisited.pop();
            }
        }
        else if(strcmp(it->second, "continue") == 0){
            //BFS
            unvisited.push(it->first);
	    while(!unvisited.empty()){
                bn = (unvisited.front());
                for(i1 = 0; i1 < (int)bn->before.size(); i1++){
                    unvisited.push(bn->before[i1]);
                }
                for(i1 = 0; i1 < (int)LoopStart.size(); i1++){
                    if(LoopStart[i1] == bn){
                        Flag = 1;
                        ((UniNode*)it->first)->next = LoopStart[i1];
                        break;
                    }
                }
                if(Flag == 1){
                    break;
                }
                visited.push(bn);
                unvisited.pop();
            }
        }
        else{
            for(label_it=LabelSet.begin(); label_it != LabelSet.end(); label_it++){
                if(strcmp(label_it->second, it->second) == 0){
                    ((UniNode*)(it->first))->next =label_it->first;
                }
            }
        }
    }
}
int exp(int x, int t){
    int i1, i2;
    i2 = 1;
    for(i1 = 0; i1 < t; i1++){
        i2 = i2 * x;
    }
    return i2;
}
string Int2String(int y){
    string r;
    r.clear();
    int i, i1, i2, x, z;
    if(y == 0){ return "0"; }
    z = y;
    if(y < 0){ x = (-1)*y; y = (-1)*y; }
    else{ x = y; }
    for(i1 = 0; y > 0; y=y/10){
        i1 = i1 + 1;
    }
    for(; i1 > 0; i1--){
        i2 = x / exp(10, i1-1);
        x = x % exp(10, i1-1);
        r = r + (char)(i2+48);
    }
    if(z < 0){  r = "-" + r; }
    return r;
}
string OPType2String(OPType l){
    string s;
    if(l == Plus){ return "+"; }
    else if(l == Minus){ return "-"; }
    else if(l == Multi){ return "*"; }
    else if(l == Divide){ return "/"; }
    else return "";
}

string Expr2String(Expr* e){
    string s;
    if(typeid(*e) == typeid(IntExpr)){
        s = Int2String(((IntExpr*)e)->i);
    }
    else if(typeid(*e) == typeid(SelectExpr)){
        s = Expr2String(((SelectExpr*)e)->a);
        s = s + "[";
        s = s + Expr2String(e);
        s = s + "]";
    }
    else if(typeid(*e) == typeid(VarExpr)){
        s = ((VarExpr*)e)->x;
    }
    else if(typeid(*e) == typeid(BinExpr)){
        s = Expr2String(((BinExpr*)e)->e1);
        s = s + OPType2String(((BinExpr*)e)->op);
        s = s + Expr2String(((BinExpr*)e)->e2);
    }
    else{
        cout << "error" << endl;
    }
    return s;
}
void CFA::SetUniNodeStatement(Node* n, int type, char *s){//type 1: assign, type 2: goto, type 3: return, type4: label, type5 funtion call
    int i1;
    char state[256];
    if(typeid(*n) == typeid(UniNode)){
        if(type == 1){
            strcpy(state, ((VarExpr*)(((UniNode*)n)->e1))->x);
            strcat(state, "=");
            strcat(state, (Expr2String(((UniNode*)n)->e2)).c_str());
        }
        else if(type == 2){
            strcpy(state, "goto ");
            strcat(state, s);
        }
        else if(type == 3){
            strcpy(state, s);
            strcat(state, " ");
            strcat(state, (Expr2String(((UniNode*)n)->e1)).c_str());
        }
        else if(type == 4){
            strcpy(state, s);
            strcat(state, ":");
        }
        else if(type == 5){
            strcpy(state, s);
            strcat(state, "(");
            for(i1 = 0; i1 < (int)((((UniNode*)n)->actualpara).size()); i1++){
                strcat(state, (Expr2String(((UniNode*)n)->actualpara[i1])).c_str());
                if(i1 != (int)((((UniNode*)n)->actualpara).size())-1){
                    strcat(state, ", ");
                }
            }
            strcat(state, ");");
        }
        else{
            cout << "error1" << endl;
        }
        strcpy(((UniNode*)n)->statement, state);
    }
    else{
        cout << "error2" << endl;
    }
}
ProgramConnectType CFA::BuildCFA(Prog prog, Node* m, Node *Term, map<Node*, char*> *gotolist){
    int i1, i2;
    i1 = 0; i2 = 0;
    Node *n = NULL;
    //InequProp *p1 = NULL;
    ProgramConnectType pct, pct1, pct2;
    vector<Node**> nodeptr1;
    vector<Node*> nodeptr2;
    //cout << "statment.size = " << prog.p.size() << endl;
    for(i1 = 0; i1 < (int)(prog.p.size()); i1++){
        cout << "prog.size = " << prog.p.size() << " i1 = " << i1;
        if(typeid(*prog.p[i1]) ==  typeid(AssignStmt)){ //assign statment
            cout << " type = Assign" << endl;
            n = new UniNode;
            ((UniNode*)n)->st=st_Assign;
        }
        else if(typeid(*prog.p[i1]) == typeid(AssertStmt)){ // assert statement
            cout << " type = Assert" << endl;
            n = new BinNode;
        }
        else if(typeid(*prog.p[i1]) == typeid(IfStmt)){ // if statment
            cout << " type = If" << endl;
            n = new BinNode;
        }
        else if(typeid(*prog.p[i1]) == typeid(WhileStmt)){ // while statment
            cout << " type = While" << endl;
            n = new BinNode;
        }
        else if(typeid(*prog.p[i1]) == typeid(GotoStmt)){ // goto statment
            cout << " type = Goto" << endl;
            n = new UniNode;
            ((UniNode*)n)->st=st_Goto;
        }
        else if(typeid(*prog.p[i1]) == typeid(LabelStmt)){ // goto statment
            cout << " type = Label" << endl;
            n = new UniNode;
            ((UniNode*)n)->st=st_Label;
        }
        else if(typeid(*prog.p[i1]) == typeid(CallFunStmt)){ // goto statment
            cout << " type = CallFun" << endl;
            n = new UniNode;
            ((UniNode*)n)->st=st_FUNC_Call;
        }
        else{
        }
        if(i1 == 0){ 
            pct.init = n;
        }
        else{
            for(i2 = 0; i2 < (int)nodeptr1.size(); i2++){
                (*nodeptr1[i2]) = n;
            }
            nodeptr1.clear();
            for(i2 = 0; i2 < (int)nodeptr2.size(); i2++){
                n->before.push_back(nodeptr2[i2]);
            }
            nodeptr2.clear();
        }
        if(typeid(*prog.p[i1]) ==  typeid(AssignStmt)){ //assign statment
            //p1 = AssignExpr2Prop(((AssignStmt*)prog.p[i1])->e1,((AssignStmt*)prog.p[i1])->e2);
            //((UniNode*)n)->p = p1;
            ((UniNode*)n)->e1 = ((AssignStmt*)prog.p[i1])->e1;
            ((UniNode*)n)->e2 = ((AssignStmt*)prog.p[i1])->e2;
            nodeptr1.push_back(&(((UniNode*)n)->next));
            nodeptr2.push_back(n);
            SetUniNodeStatement(n, 1, NULL);
        }
        else if(typeid(*prog.p[i1]) == typeid(AssertStmt)){ // assert statement
            ((BinNode*)n)->p = ((AssertStmt*)prog.p[i1])->p;
            nodeptr1.push_back(&(((BinNode*)n)->_true));
            nodeptr2.push_back(n);
            ((BinNode*)n)->_false = m;
        }
        else if(typeid(*prog.p[i1]) == typeid(IfStmt)){ // if statment
            ((BinNode*)n)->p = ((IfStmt*)prog.p[i1])->p;
            if(((IfStmt*)prog.p[i1])->p1 != NULL){
                pct1 = BuildCFA(*(((IfStmt*)prog.p[i1])->p1), m, Term, gotolist);
                ((BinNode*)n)->_true = ((pct1.init));
                pct1.init->before.push_back(n);
                for(i2 = 0; i2 < (int)pct1.ends1.size(); i2++){
                    nodeptr1.push_back(pct1.ends1[i2]);
                }
                for(i2 = 0; i2 < (int)pct1.ends2.size(); i2++){
                    nodeptr2.push_back(pct1.ends2[i2]);
                }
            }
            if(((IfStmt*)prog.p[i1])->p2 != NULL){
                pct2 = BuildCFA(*(((IfStmt*)prog.p[i1])->p2), m, Term, gotolist);
                ((BinNode*)n)->_false = ((pct2.init));
                pct2.init->before.push_back(n);
                for(i2 = 0; i2 < (int)pct2.ends1.size(); i2++){
                    nodeptr1.push_back(pct2.ends1[i2]);
                }
                for(i2 = 0; i2 < (int)pct2.ends2.size(); i2++){
                    nodeptr2.push_back(pct2.ends2[i2]);
                }
            }
            else{
                //
                nodeptr1.push_back(&(((BinNode*)n)->_false));
                nodeptr2.push_back(n);
            }
        }
        else if(typeid(*prog.p[i1]) == typeid(WhileStmt)){ // while statment
            ((BinNode*)n)->p = (((WhileStmt*)prog.p[i1])->p);
            pct1 = BuildCFA(*(((IfStmt*)prog.p[i1])->p1), m, Term, gotolist);
            ((BinNode*)n)->_true = (pct1.init);
            pct1.init->before.push_back(n);
            nodeptr1.push_back(&(((BinNode*)n)->_false));
            for(i2 = 0; i2 < (int)pct1.ends1.size(); i2++){
                *(pct1.ends1[i2]) = n;
            }
            nodeptr2.push_back(n);
            LoopStart.push_back(n);
            LoopEnd.push_back(&(((BinNode*)n)->_false));
            /*for(i2 = 0; i2 < (int)pct1.ends2.size(); i2++){
                nodeptr2.push_back(pct1.ends2[i2]);
            }*/
        }
        else if(typeid(*prog.p[i1]) == typeid(GotoStmt)){ // Goto statment
            ((UniNode*)n)->e1 = NULL;
            ((UniNode*)n)->e2 = NULL;
            //nodeptr1.push_back(&(((UniNode*)n)->next));// this is not right
            if(strcmp(((GotoStmt*)prog.p[i1])->L, "continue") != 0 && strcmp(((GotoStmt*)prog.p[i1])->L,"break") != 0 && strcmp(((GotoStmt*)prog.p[i1])->L,"return") != 0){
                gotolist->insert(pair<Node*, char*>(n, ((GotoStmt*)prog.p[i1])->L));
                //strcpy(((UniNode*)n)->statement, ((GotoStmt*)(prog.p[i1]))->L);
                SetUniNodeStatement(n, 2, ((GotoStmt*)(prog.p[i1]))->L);
            }
            else if(strcmp(((GotoStmt*)prog.p[i1])->L, "continue") == 0){
                gotolist->insert(pair<Node*, char*>(n, ((GotoStmt*)prog.p[i1])->L));
                strcpy(((UniNode*)n)->statement, ((GotoStmt*)(prog.p[i1]))->L);
                //SetUniNodeStatement(n, 3, "continue");
            }
            else if(strcmp(((GotoStmt*)prog.p[i1])->L, "break") == 0){
                gotolist->insert(pair<Node*, char*>(n, ((GotoStmt*)prog.p[i1])->L));
                strcpy(((UniNode*)n)->statement, ((GotoStmt*)(prog.p[i1]))->L);
                //SetUniNodeStatement(n, 3, "break");
            }
            else if(strcmp(((GotoStmt*)prog.p[i1])->L, "return") == 0){
                ((UniNode*)n)->next = Term;
                //strcpy(((UniNode*)n)->statement, ((GotoStmt*)(prog.p[i1]))->L);
                ((UniNode*)n)->e1 = ((GotoStmt*)(prog.p[i1]))->e;
                SetUniNodeStatement(n, 3, ((GotoStmt*)prog.p[i1])->L);
            }
            else{
            }
            nodeptr2.push_back(n);
        }
        else if(typeid(*prog.p[i1]) == typeid(LabelStmt)){ // Label statment
            ((UniNode*)n)->e1 = NULL;
            ((UniNode*)n)->e2 = NULL;
            LabelSet.insert( pair<Node*, char*>(n, ((LabelStmt*)(prog.p[i1]))->L) );
            //strcpy(((UniNode*)n)->statement, ((LabelStmt*)(prog.p[i1]))->L);
            SetUniNodeStatement(n, 4, ((LabelStmt*)(prog.p[i1]))->L);
            nodeptr1.push_back(&(((UniNode*)n)->next));
            nodeptr2.push_back(n);
        }
        else if(typeid(*prog.p[i1]) == typeid(CallFunStmt)){ // Label statment
            ((UniNode*)n)->e1 = NULL;
            ((UniNode*)n)->e2 = NULL;
            strcpy(((UniNode*)n)->name, ((CallFunStmt*)(prog.p[i1]))->fun);
            ((UniNode*)n)->actualpara = ((CallFunStmt*)(prog.p[i1]))->para;
            SetUniNodeStatement(n, 5, ((CallFunStmt*)(prog.p[i1]))->fun);
            nodeptr1.push_back(&(((UniNode*)n)->next));
            nodeptr2.push_back(n);
        }
        else{
        }
    }
    pct.ends1 = nodeptr1;
    pct.ends2 = nodeptr2;
    return pct;
}
void CFA::PrintLogicType(LogicType l){
    if(l == And){ cout << "&&"; }
    else if(l == Or){ cout << "||"; }
    else{ }
}
void CFA::PrintProp(Prop* p){
    if(typeid(*p) == typeid(BoolProp)){
        if(((BoolProp*)p)->b == true){ cout << "TRUE"; }
        else{ cout << "FALSE"; }
    }
    else if(typeid(*p) == typeid(NegProp)){
        cout << "~ ";
        PrintProp(((NegProp*)p)->p);
    }
    else if(typeid(*p) == typeid(BinProp)){
        PrintProp(((BinProp*)p)->p1);
        PrintLogicType(((BinProp*)p)->l);
        PrintProp(((BinProp*)p)->p2);
    }
    else if(typeid(*p) == typeid(InequProp)){
        PrintExpr(((InequProp*)p)->e1);
        PrintPropType(((InequProp*)p)->p);
        PrintExpr(((InequProp*)p)->e2);
    }
    else{
        cout << "error" << endl;
    }
}
void CFA::PrintOPType(OPType l){
    if(l == Plus){ cout << "+"; }
    else if(l == Minus){ cout << "-"; }
    else if(l == Multi){ cout << "*"; }
    else if(l == Divide){ cout << "/"; }
    else{ }
}
void CFA::PrintPropType(PropType l){
    if(l == LT){ cout << "<"; }
    else if(l == GT){ cout << ">"; }
    else if(l == Eq){ cout << "=="; }
    else{ }
}
void CFA::PrintExpr(Expr* e){
    if(typeid(*e) == typeid(IntExpr)){
        cout << ((IntExpr*)e)->i;
    }
    else if(typeid(*e) == typeid(SelectExpr)){
        cout << Expr2String(((SelectExpr*)e)->a) << "[";
        PrintExpr(e);
        cout << "]";
    }
    else if(typeid(*e) == typeid(VarExpr)){
        cout << ((VarExpr*)e)->x;
    }
    else if(typeid(*e) == typeid(BinExpr)){
        PrintExpr(((BinExpr*)e)->e1);
        PrintOPType(((BinExpr*)e)->op);
        PrintExpr(((BinExpr*)e)->e2);
    }
    else{
        cout << "error" << endl;
    }
}
void CFA::PrintNode(Node* n){
    if(n == NULL){
        cout << "terminalNode" << endl;
    }
    else if(typeid(*n) == typeid(UniNode)){
        cout << "UniNode!!! " << " "; 
        //PrintProp(((UniNode*)n)->p);
        if(((UniNode*)n)->e1 == NULL && ((UniNode*)n)->e2 == NULL){
            cout << ((UniNode*)n)->statement;
        }
        else{ 
	    PrintExpr(((UniNode*)n)->e1);
            cout << "=";
            PrintExpr(((UniNode*)n)->e2);
        }
        //cout <<((UniNode*)n)->GetNext() << endl;
        //printf("%d\n", ((UniNode*)n)->GetNext());
        //PrintProp(((UniNode*)n)->GetNext()->GetP());
        /*if(typeid(*(((UniNode*)n)->next)) == typeid(UniNode) ){
            cout << endl; cout << ", Next = ";
            //PrintProp(((UniNode*)((UniNode*)n)->next)->p);
            PrintExpr(((UniNode*)(((UniNode*)n)->next))->e1);
            cout << "=";
            PrintExpr(((UniNode*)(((UniNode*)n)->next))->e2);
        }
        else if(typeid(*((UniNode*)n)->next) == typeid(BinNode)){
            cout << endl << ", Next1 = ";
            PrintProp(((BinNode*)(((UniNode*)n)->next))->p);
        }
        else{
            cout << endl << ", Next1 = terminal";
        }*/
        //只印內容
        cout << endl;
    }
    else if(typeid(*n) == typeid(BinNode)){
        cout << "BinNode!!! " << " "; 
        PrintProp(((BinNode*)n)->p);
        /*if(typeid(*((BinNode*)n)->_true) == typeid(UniNode) ){
            cout << endl << ", Next1 = ";
            //PrintProp(((UniNode*)((BinNode*)n)->_true)->p);
            PrintExpr(((UniNode*)((BinNode*)n)->_true)->e1);
            cout << "=";
            PrintExpr(((UniNode*)((BinNode*)n)->_true)->e2);
        }
        else if(typeid(*((BinNode*)n)->_true) == typeid(BinNode)){
            cout << endl << ", Next1 = ";
            PrintProp(((BinNode*)(((BinNode*)n)->_true))->p);
        }
        else{
            cout << endl << ", Next1 = terminal";
        }
        if(typeid(*((BinNode*)n)->_false) == typeid(UniNode) ){
            cout << endl << ", Next2 = ";
            //PrintProp(((BinNode*)((BinNode*)n)->_false)->p);
            PrintExpr(((UniNode*)((BinNode*)n)->_false)->e1);
            cout << "=";
            PrintExpr(((UniNode*)((BinNode*)n)->_false)->e2);
        }
        else if(typeid(*((BinNode*)n)->_false) == typeid(BinNode)){
            cout << endl << ", Next2 = ";
            PrintProp(((BinNode*)(((BinNode*)n)->_false))->p);
        }
        else if(typeid(*n) == typeid(BadNode)){
            cout << ", Next2 = BadNode" << endl;
        }
        else{
            cout << endl << ", Next2 = terminal";
        }*/
        //只印內容
        cout << endl;
    }
    else if(typeid(*n) == typeid(BadNode)){
        cout << "BadNode" << endl;
    }
    else{
    }

}
bool CFA::IsFound(vector<Node*> *visit, Node* X){
    //PrintNode(X);
    int i1;
    bool result;
    i1 = 0; result = false;
    for(i1 = 0; i1 < (int)visit->size(); i1++){
        if((*visit)[i1] == X){ result = true; }
    }
    return result;
}
void CFA::RecursiveVerifyNode(Node* X, set<Node*>& visit){
    if(visit.find(X) != visit.end()){ return; }
    //cout << "X = " << X << endl;
    PrintNode(X);
    visit.insert(X);
    if(typeid(*X) == typeid(UniNode)){ 
        RecursiveVerifyNode(((UniNode*)X)->next, visit);
    }
    else if(typeid(*X) == typeid(BinNode)){
        RecursiveVerifyNode(((BinNode*)X)->_true, visit);
        RecursiveVerifyNode(((BinNode*)X)->_false, visit);   
    }
    else{ return; }
}
void CFA::PrintCFA(){
    int i1;
    i1 = 0;
    set<Node*> visit;
    RecursiveVerifyNode(GetInitNode(), visit);
}
void CFA::PrintBackNode(Node* n){
    int i1;
    i1 = 0;
    for(i1 = 0; i1 < (int)n->before.size(); i1++){
        //if(typeid(*n) == typeid(UniNode)){ PrintProp(((UniNode*)n)->p); }
        if(n == NULL){ cout << "TermNode"; }
        else if(typeid(*n) == typeid(UniNode)){ PrintExpr(((UniNode*)n)->e1); cout << "="; PrintExpr(((UniNode*)n)->e2); }
        else if(typeid(*n) == typeid(BinNode)){ PrintProp(((BinNode*)n)->p); }
        else if(typeid(*n) == typeid(BadNode)){ cout << "BadNode" ; }
        else{ }
        cout << " -> ";
        //cout << n->before[i1] << endl;
        //if(typeid(*(n->before[i1])) == typeid(UniNode)){ PrintProp(((UniNode*)(n->before[i1]))->p); }
        if(n->before[i1] == NULL){ cout << "Terminal"; }
        else if(typeid(*(n->before[i1])) == typeid(UniNode)){ 
            PrintExpr(((UniNode*)(n->before[i1]))->e1); cout << "="; PrintExpr(((UniNode*)(n->before[i1]))->e2);}
        else if(typeid(*(n->before[i1])) == typeid(BinNode)){ PrintProp(((BinNode*)(n->before[i1]))->p); }
        else if(typeid(*(n->before[i1])) == typeid(BadNode)){ cout << "BadNode"; }
        else{ }
        cout << endl;
    }
}
void CFA::RecursiveVerifyBackNode(Node* X, set<Node*> &visit){
    int i2;
    i2 = 0;
    if(visit.find(X) != visit.end()){ return; }
    PrintBackNode(X);
    visit.insert(X);
    for(i2 = 0; i2 < (int)X->before.size(); i2++){
        RecursiveVerifyBackNode(X->before[i2], visit);
    }
}
void CFA::PrintBackCFA(){
    int i1;
    i1 = 0;
    set<Node*> visit;
    RecursiveVerifyBackNode(GetFinalNode(), visit);
}
void CFA::BuildGraph(int i1){
    ProgramConnectType pct;
    map<Node*, char*> gotolist;
    Node* m;
    m = new BadNode;
    //cout << "size = " << fun.size() << " i1 = " << i1 << endl;
    //pct = BuildCFA(*(fun[i1]), m, NULL, &gotolist);
    //pct = BuildCFA(*prog1, m);
    ConnectGoto(&gotolist);
    SetInitNode(pct.init);
    //strcpy(id, fun[i1]->name);
    //formal_parameter = fun[i1]->formal_para;
    for(i1 = 0; i1 < (int)pct.ends1.size(); i1++){
        (*(pct.ends1[i1])) = NULL;
    }
}
void CFA::GraphOPType(ofstream &out, OPType l){
    if(l == Plus){ out << "+"; }
    else if(l == Minus){ out << "-"; }
    else if(l == Multi){ out << "*"; }
    else if(l == Divide){ out << "/"; }
    else{ }
}
void CFA::GraphExpr(ofstream &out, Expr *e){
    if(typeid(*e) == typeid(IntExpr)){
        out << ((IntExpr*)e)->i;
    }
    else if(typeid(*e) == typeid(SelectExpr)){
        out << Expr2String(((SelectExpr*)e)->a) << "[";
        GraphExpr(out, e);
        out << "]";
    }
    else if(typeid(*e) == typeid(VarExpr)){
        out << ((VarExpr*)e)->x;
    }
    else if(typeid(*e) == typeid(BinExpr)){
        GraphExpr(out, ((BinExpr*)e)->e1);
        GraphOPType(out, ((BinExpr*)e)->op);
        GraphExpr(out, ((BinExpr*)e)->e2);
    }
    else{
        out << "error" << endl;
    }
}
void CFA::GraphLogicType(ofstream &out, LogicType l){
    if(l == And){ out << "&&"; }
    else if(l == Or){ out << "||"; }
    else{ }
}
void CFA::GraphPropType(ofstream &out, PropType l){
    if(l == LT){ out << "<"; }
    else if(l == GT){ out << ">"; }
    else if(l == Eq){ out << "=="; }
    else{ }
}
void CFA::GraphProp(ofstream &out, Prop *p){
    if(typeid(*p) == typeid(BoolProp)){
        if(((BoolProp*)p)->b == true){ out << "TRUE"; }
        else{ out << "FALSE"; }
    }
    else if(typeid(*p) == typeid(NegProp)){
        out << "~(";
        GraphProp(out, ((NegProp*)p)->p);
	out<<")";
    }
    else if(typeid(*p) == typeid(BinProp)){
        GraphProp(out, ((BinProp*)p)->p1);
        GraphLogicType(out, ((BinProp*)p)->l);
        GraphProp(out, ((BinProp*)p)->p2);
    }
    else if(typeid(*p) == typeid(InequProp)){
        GraphExpr(out,((InequProp*)p)->e1);
        GraphPropType(out, ((InequProp*)p)->p);
        GraphExpr(out, ((InequProp*)p)->e2);
    }
    else{
        out << "error" << endl;
    }
}
void CFA::GraphNode(ofstream &out, Node* n, set<Node*> &visit){
    if(n == NULL){
        return;
    }
    else if(typeid(*n) == typeid(UniNode)){   
        out << "\"" << ((UniNode*)n)->statement << "(#" << n << ")" << "\"";
        if(((UniNode*)n)->next == NULL){
            out << " -> \"terminal\"";
        }
        else if(typeid(*(((UniNode*)n)->next)) == typeid(UniNode) ){
            out << " -> ";
            out << "\"" << ((UniNode*)(((UniNode*)n)->next))->statement;
            out << "(#" << ((UniNode*)n)->next << ")";
            out << "\"";
        }
        else if(typeid(*((UniNode*)n)->next) == typeid(BinNode)){
            out << " -> ";
            out << "\"";
            GraphProp(out, ((BinNode*)(((UniNode*)n)->next))->p);
            out << "(#" << ((UniNode*)n)->next << ")";
            out << "\"";
        }
        else{
        }
        out << ";" << endl;
    }
    else if(typeid(*n) == typeid(BinNode)){
        out << "\"";
        GraphProp(out, ((BinNode*)n)->p);
        out << "(#" << n << ")";
        out << "\"";
        if(((BinNode*)n)->_true == NULL){
            out << " -> \"terminal\"";
        }
        else if(typeid(*(((BinNode*)n)->_true)) == typeid(UniNode) ){
            out << " -> ";
            out << "\"" << ((UniNode*)(((BinNode*)n)->_true))->statement;
            out << "(#" << ((BinNode*)n)->_true << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_true) == typeid(BinNode)){
            out << " -> ";
            out << "\"";
            GraphProp(out, ((BinNode*)((BinNode*)n)->_true)->p);
            out << "(#" << ((BinNode*)n)->_true << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_true) == typeid(BadNode)){
            out << " -> \"BadNode\"";
        }
        else{
        }
        out << "[label = \"Y\"]";
        out << ";" << endl;
        out << "\"";
        GraphProp(out, ((BinNode*)n)->p);
        out << "(#" << n << ")";
        out << "\"";
        if(((BinNode*)n)->_false == NULL){
            out << "-> \"terminal\"";
        } 
        else if(typeid(*(((BinNode*)n)->_false)) == typeid(UniNode) ){
            out << " -> ";
            out << "\"" << ((UniNode*)(((BinNode*)n)->_false))->statement;
            out << "(#" << ((BinNode*)n)->_false << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_false) == typeid(BinNode)){
            out << " -> ";
            out << "\"";
            GraphProp(out, ((BinNode*)((BinNode*)n)->_false)->p);
            out << "(#" << ((BinNode*)n)->_false << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_false) == typeid(BadNode)){
            out << "-> \"BadNode\"";
        }
        else{
        }
        out << "[label = \"N\"]";
        out << ";" << endl;
    }
    else{
    }
}
void CFA::RecursiveGraphNode(ofstream& out, Node *X, set<Node*> &visit){
    if(visit.find(X) != visit.end()){ return; }
    visit.insert(X);
    GraphNode(out, X, visit);
    if(X == NULL){
        return;
    }
    else if(typeid(*X) == typeid(UniNode)){
        RecursiveGraphNode(out, ((UniNode*)X)->next, visit);
    }
    else if(typeid(*X) == typeid(BinNode)){
        RecursiveGraphNode(out, ((BinNode*)X)->_true, visit);
        RecursiveGraphNode(out, ((BinNode*)X)->_false, visit);
    }
    else{
        return;
    }
}
void CFA::PrintSingleNodeWithGraphviz(ofstream &out, Node* n){
    if(n == NULL){
        out << "\"TermNode\"";
    }
    else if(typeid(*n) == typeid(UniNode)){
        out << "\"" << ((UniNode*)n)->statement << "\"";
    }
    else if(typeid(*n) == typeid(BinNode)){
        out << "\""; GraphProp(out, ((BinNode*)n)->p); out << "\"";
    }
    else if(typeid(*n) == typeid(BadNode)){
        out << "\"BadNode\"";
    }
    else{
    }
}
void CFA::GraphNode1(ofstream &out, Node* n, set<Node*> &visit, int x, int y){
    if(typeid(*n) == typeid(UniNode)){
        out << "s" << visit.size() << "[shape=ellipse, label=";
        PrintSingleNodeWithGraphviz(out, ((UniNode*)n)->next);
        out << ", pos=\"" << x << "," << y-1 << "!\"];" << endl;
        out << "s" << visit.size()-1 << " -- s" << visit.size() << ";" << endl;
    }
    else if(typeid(*n) == typeid(BinNode)){
        out << "\"";
        GraphProp(out, ((BinNode*)n)->p);
        out << "(#" << n << ")";
        out << "\"";
        if(((BinNode*)n)->_true == NULL){
            out << " -> \"terminal\"";
        }
        else if(typeid(*(((BinNode*)n)->_true)) == typeid(UniNode) ){
            out << " -> ";
            out << "\"";
            //GraphProp(out, ((UniNode*)((BinNode*)n)->_true)->p);
            GraphExpr(out, ((UniNode*)((BinNode*)n)->_true)->e1); out << "=";
            GraphExpr(out, ((UniNode*)((BinNode*)n)->_true)->e2);
            out << "(#" << ((BinNode*)n)->_true << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_true) == typeid(BinNode)){
            out << " -> ";
            out << "\"";
            GraphProp(out, ((BinNode*)((BinNode*)n)->_true)->p);
            out << "(#" << ((BinNode*)n)->_true << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_true) == typeid(BadNode)){
            out << " -> \"BadNode\"";
        }
        else{
        }
        out << "[label = \"Y\"]";
        out << ";" << endl;
        out << "\"";
        GraphProp(out, ((BinNode*)n)->p);
        out << "(#" << n << ")";
        out << "\"";
        if(((BinNode*)n)->_false == NULL){
            cout << "-> \"terminal\"" << endl;
        } 
        else if(typeid(*(((BinNode*)n)->_false)) == typeid(UniNode) ){
            out << " -> ";
            out << "\"";
            //GraphProp(out, ((UniNode*)((BinNode*)n)->_false)->p);
            GraphExpr(out, ((UniNode*)((BinNode*)n)->_false)->e1); out << "=";
            GraphExpr(out, ((UniNode*)((BinNode*)n)->_false)->e2);
            out << "(#" << ((BinNode*)n)->_false << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_false) == typeid(BinNode)){
            out << " -> ";
            out << "\"";
            GraphProp(out, ((BinNode*)((BinNode*)n)->_false)->p);
            out << "(#" << ((BinNode*)n)->_false << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_false) == typeid(BadNode)){
            cout << "-> \" BadNode\"" << endl;
        }
        else{
        }
        out << "[label = \"N\"]";
        out << ";" << endl;
    }
    else{
    }
}

void CFA::RecursiveGraphNode1(ofstream& out, Node *X, set<Node*> &visit, int x, int y){
    if(visit.find(X) != visit.end()){ return; }
    visit.insert(X);
    GraphNode1(out, X, visit, x, y);
    if(typeid(*X) == typeid(UniNode)){
        RecursiveGraphNode1(out, ((UniNode*)X)->next, visit, x, y-1);
    }
    else if(typeid(*X) == typeid(BinNode)){
        RecursiveGraphNode1(out, ((BinNode*)X)->_true, visit, x-6, y-1);
        RecursiveGraphNode1(out, ((BinNode*)X)->_false, visit, x+6, y-1);
    }
    else{
        return;
    }
}
void CFA::CFA2Dot(const char *outputName){
    int i1;
    i1 = 0;
    ofstream out(outputName);
    set<Node*> visit;
    //out << "graph G {" << endl << "[overlap=false];" << endl;
    //out << "s0[label="; PrintSingleNodeWithGraphviz(out, GetInitNode()); out << ",pos=\"0.0,0.0!\"];" << endl;
    out << "digraph G {" << endl;
    RecursiveGraphNode(out, initNode, visit);
    //RecursiveGraphNode1(out, initNode, visit, 0, 0);
    out << "}";
}
